Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
Identifieur interne : 008796 ( Main/Exploration ); précédent : 008795; suivant : 008797Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
Auteurs : David Déharbe [Brésil] ; Anamaria Martins Moreira [Brésil] ; Christophe Ringeissen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract: A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NF-CTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NF-CTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.
Url:
DOI: 10.1007/3-540-45610-4_15
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000D59
- to stream Istex, to step Curation: 000D50
- to stream Istex, to step Checkpoint: 001C32
- to stream Main, to step Merge: 008C52
- to stream PascalFrancis, to step Corpus: 000785
- to stream PascalFrancis, to step Curation: 000258
- to stream PascalFrancis, to step Checkpoint: 000803
- to stream Main, to step Merge: 008D88
- to stream Main, to step Curation: 008796
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name></author><author><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:395EAC54F49E719F8819BA68AAF9829935FAE91C</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45610-4_15</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-1QL06KCC-3/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000D59</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000D59</idno><idno type="wicri:Area/Istex/Curation">000D50</idno><idno type="wicri:Area/Istex/Checkpoint">001C32</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C32</idno><idno type="wicri:doubleKey">0302-9743:2002:Deharbe D:improving:symbolic:model</idno><idno type="wicri:Area/Main/Merge">008C52</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:03-0333782</idno><idno type="wicri:Area/PascalFrancis/Corpus">000785</idno><idno type="wicri:Area/PascalFrancis/Curation">000258</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000803</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000803</idno><idno type="wicri:doubleKey">0302-9743:2002:Deharbe D:improving:symbolic:model</idno><idno type="wicri:Area/Main/Merge">008D88</idno><idno type="wicri:Area/Main/Curation">008796</idno><idno type="wicri:Area/Main/Exploration">008796</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae</title><author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name><affiliation wicri:level="2"><country xml:lang="fr">Brésil</country><wicri:regionArea>Universidade Federal do Rio Grande do Norte — UFRN, Natal, RN</wicri:regionArea><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name><affiliation wicri:level="2"><country xml:lang="fr">Brésil</country><wicri:regionArea>Universidade Federal do Rio Grande do Norte — UFRN, Natal, RN</wicri:regionArea><placeName><region type="state">Rio Grande do Norte</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Brésil</country></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm complexity</term><term>Formal verification</term><term>Logic model</term><term>Model checking</term><term>Program verification</term><term>Rewriting systems</term><term>Temporal logic</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Complexité algorithme</term><term>Logique arbre calcul point fixe</term><term>Logique temporelle</term><term>Modèle logique</term><term>Système réécriture</term><term>Vérification formelle</term><term>Vérification programme</term><term>Vérification énumérative</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula f, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NF-CTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NF-CTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.</div></front></TEI><affiliations><list><country><li>Brésil</li><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Rio Grande do Norte</li></region><settlement><li>Nancy</li></settlement></list><tree><country name="Brésil"><region name="Rio Grande do Norte"><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name></region><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name><name sortKey="Moreira, Anamaria Martins" sort="Moreira, Anamaria Martins" uniqKey="Moreira A" first="Anamaria Martins" last="Moreira">Anamaria Martins Moreira</name></country><country name="France"><region name="Grand Est"><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></region><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008796 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008796 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:395EAC54F49E719F8819BA68AAF9829935FAE91C
|texte= Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae
}}
| This area was generated with Dilib version V0.6.33. |  |